<html>
<head><meta charset="utf-8"><title>CDCL terminology · t-cargo/PubGrub · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/260232-t-cargo/PubGrub/index.html">t-cargo/PubGrub</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/260232-t-cargo/PubGrub/topic/CDCL.20terminology.html">CDCL terminology</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="214907170"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260232-t-cargo/PubGrub/topic/CDCL%20terminology/near/214907170" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Matthieu Pizenberg <a href="https://rust-lang.github.io/zulip_archive/stream/260232-t-cargo/PubGrub/topic/CDCL.20terminology.html#214907170">(Oct 28 2020 at 22:49)</a>:</h4>
<p>While writing the guide on internals, I want to make a clear link between PubGrub terminology and CDCL (conflict driven clause learning) terminology. It is clear that terms correspond to literals, but it's less clear what incompatibilities are. I would tend to say that they correspond to clauses, but clauses rather seems to be the opposite of incompatibilities. While a clause is a disjunction that should have at least one literal evaluated true, incompatibilities are conjunctions that must evaluate to false (have at least one literal that is false).</p>



<a name="214907256"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260232-t-cargo/PubGrub/topic/CDCL%20terminology/near/214907256" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Matthieu Pizenberg <a href="https://rust-lang.github.io/zulip_archive/stream/260232-t-cargo/PubGrub/topic/CDCL.20terminology.html#214907256">(Oct 28 2020 at 22:50)</a>:</h4>
<p>Do any of you know why PubGrub decided to work with incompatibilities instead of clauses like it's done in traditional CDCL?</p>



<a name="214909382"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260232-t-cargo/PubGrub/topic/CDCL%20terminology/near/214909382" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Eh2406 <a href="https://rust-lang.github.io/zulip_archive/stream/260232-t-cargo/PubGrub/topic/CDCL.20terminology.html#214909382">(Oct 28 2020 at 23:16)</a>:</h4>
<p>I think that reframing comes from the "Answer Set Solving" authors.</p>



<a name="214909421"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260232-t-cargo/PubGrub/topic/CDCL%20terminology/near/214909421" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Matthieu Pizenberg <a href="https://rust-lang.github.io/zulip_archive/stream/260232-t-cargo/PubGrub/topic/CDCL.20terminology.html#214909421">(Oct 28 2020 at 23:17)</a>:</h4>
<p>Ah I think I found the reason. PubGrub is actually mostly inspired by Potassco (<a href="https://potassco.org/teaching/">https://potassco.org/teaching/</a>) and there, incompatibilities are called "nogoods" and the algorithm is called CDNL for conflict driven nogood learning instead of CDCL</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>